Skip to content

Conversation

@purefunctor
Copy link
Owner

This changes the representation of Variable::Bound to carry its kind similar to Variable::Skolem. Tests have been updated to verbosely pretty-print the kinds of both bound and skolem type variables.

See TODO comment in changes. This requires further changes such that we
can more accurately describe the kind of a bound type variable found in
an instance declaration's constraints. For now, using a  unification
variable should suffice and allows the tests to be solved.
This makes us less reliant on the implicit scope when transferring types
across the global/local contexts. This also removes the workaround in
constraint.rs that uses unification variables to stand in for the erased
kind information important for correctness.
@purefunctor purefunctor merged commit a95a16b into main Jan 17, 2026
10 checks passed
@purefunctor purefunctor deleted the justin/embed-bound-kind branch January 17, 2026 05:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants